-module(prop_cfr).
-include_lib("proper/include/proper.hrl").
-include("../src/rtps.hrl").
-include("../src/rtps_cfr.hrl").

dds_filter(_Seq_num) ->
    true.

%%%%%%%%%%%%%%%%%%
%%% Properties %%%
%%%%%%%%%%%%%%%%%%
prop_init() ->
    ?FORALL({Min_seq_num, N, Push_mode}, {seq_num(pos_integer()), non_neg_integer(), boolean()},
        begin
	    %% We get a lost, at least one or more received and an unknown cfrs.
	    Cfrs = rtps_cfr:new(Min_seq_num, Min_seq_num + N, fun dds_filter/1, Push_mode),
	    check_struct_cfrs(Cfrs, N)
	end).


%%%%%%%%%%%%%%%
%%% Helpers %%%
%%%%%%%%%%%%%%%

%% Check overall structure of the cfrs list. N is the number of cfrs the list manages.
check_struct_cfrs(Cfrs, N) ->
	length(Cfrs) =:= N + 1.
	
%%%%%%%%%%%%%%%%%%
%%% Generators %%%
%%%%%%%%%%%%%%%%%%
seq_num(Gen) ->
    ?SUCHTHAT(N, Gen, N =/= undefined).
